\begin{tabbing} $\forall$${\it es}$:event\_system\{i:l\}, $e_{1}$,$e_{2}$:es{-}E(${\it es}$), $P$:(\=\{$e$:es{-}E(${\it es}$)$\mid$ loc($e$) = loc($e_{1}$) $\in$ Id\} $\rightarrow$\+ \\[0ex]prop\{i:l\}). \-\\[0ex](loc($e_{2}$) = loc($e_{1}$) $\in$ Id) $\Rightarrow$ ($\forall$$e$$\in$[$e_{1}$,$e_{2}$].$P$($e$) $\in$ prop\{i:l\}) \end{tabbing}